D:Dsys, i:Id. Feasible(D)  AtomFree(ds(M(i))) 

latex

Definitions	x:A. B(x), P  Q, t  T, Feasible(D), P & Q, Feasible(M), ma-frame-compat(A;B), Prop, AtomFree(d), ds(M)
Lemmas	d-feasible wf, Id wf, dsys wf